Nuprl Lemma : strong-subtype-equal
0,22
postcript
pdf
A
,
B
:Type.
A
=
B
strong-subtype(
A
;
B
)
latex
Definitions
P
Q
,
Prop
,
strong-subtype(
A
;
B
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
strong-subtype
wf
,
strong-subtype-self
origin
A, B:Type. A = B 
strong-subtype(A;B) A, B:Type. A = B strong-subtype(A;B) Qx:A. B(x)
T